FDL - Nuprl Lemma : ma-random-sub

Nuprl Lemma : ma-random-sub

M1, M2:MsgA.
M1

i, a:Id, T:Type, v:T, n:

. ma-random(M2;T;v;i;a;n)

ma-random(M1;T;v;i;a;n))

Definitions	t T, Id, Atom$n, P Q, False, A, A B, , {x:A\| B(x)} , , x:AB(x), x:A. B(x), x. t(x), FinProbSpace, f(x), random(p;a;b), f(a), A c B, x:A B(x), <a, b>, s = t, Outcome, , b, f g, Knd, IdLnk, z != f(x) P(a;z), P & Q, Valtype(da;k), MsgA, M1 M2, ma-random(M;T;v;i;a;n), Type
Lemmas	p-outcome wf, random wf, fpf-ap wf